\begin{tabbing}
$\forall$$A$,$B$:es\_realizer\{i:l\}.
\\[0ex]R{-}interface($A$; $B$)
\\[0ex]$\Leftarrow\!\Rightarrow$ \=($\forall$$i$:Id. \+
\\[0ex]($\uparrow$R{-}has{-}loc($B$; $i$))
\\[0ex]$\Rightarrow$ fpf{-}all(\=Knd;\+
\\[0ex]Kind{-}deq;
\\[0ex]R{-}da($B$; $i$);
\\[0ex]$k$,$T$.(($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ (destination(lnk($k$)) = $i$ $\in$ Id)
\\[0ex]$\Rightarrow$ subtype\_rel(fpf{-}cap(R{-}da($A$; source(lnk($k$))); Kind{-}deq; $k$; void); $T$))))
\-\-
\end{tabbing}